00100	                      SOME NEW RULES FOR PCHECK
00200	
00300	
00400		This memo documents a collection of commands for  PCHECK  and
00500	should  be read only by those familiar with Diffie's proof checker as
00600	described in PCHECK.DOC[DOC,WD].  This  group  of  commands  generate
00700	assertions  about S-expressions.  As it happens, none of the commands
00800	are rules of inference in the sense of taking previous  sentences  as
00900	premises.   They  are  rather  axiom  generators.  More will be added
01000	later.
01100	
01200	
01300	EValuateCAR(s-expression)
01400		If the argument is not a quoted S-expression, no new line  is
01500	generated.    If   the  argument  is  a  quoted  atom,  then  a  line
01600	s-expression=UU is generated.  If the argument is a quoted non-atomic
01700	S-expression,  then  a  line  CAR(s-expression)='car[s-expression] is
01800	generated.  Thus, EVCAR(A) produces no result, EVCAR('A) produces
01900		CAR('A)=UU and EVCAR('(A B)) produces
02000		CAR('(A B))='A.
02100	
02200	EValuateCDR(s-expression)
02300		EVCDR is similar to EVCAR with the obvious difference.
02400	
02500	EValuateCONS(sexp1,sexp2)
02600		If not both sexp1 and sexp2 are quoted S-expressions,  EVCONS
02700	does nothing.  Otherwise, it generates a sentence of the form
02800		CONS(sexp1,sexp2)=cons[sexp1,sexp2].    Thus    EVCONS('A,'B)
02900	generates
03000		CONS('A,'B)='(A.B).
03100	
03200	EValuateEQUAL(sexp1,sexp2)
03300		EVEQUAL(sexp1,sexp2)  asserts  the  equality or inequality of
03400	two quoted S-expressions.  Thus EVEQUAL('(A B),'(A B)) generates
03500		'(A B)='(A B) and EVEQUAL('A,'B) generates
03600		¬('A='B).
03700	
03800	EValuateATOM(sexp)
03900		EVATOM(sexp)  tells  us  whether  sexp is atomic.  EVATOM('A)
04000	generates
04100		ATOM('A) and EVATOM('(A B)) generates
04200		¬ATOM('(A B)).
04300	
04400	ISSEXPression(sexp)
04500		ISSEXP(sexp)  asserts that its argument is an S-expression if
04600	it is a quoted S-expression.  Thus ISSEXP('A) generates
04700		ISSEXP('A)  while  ISSEXP(A)  does not generated a line since
04800	the value of A may or may not be an S-expression.
04900	
05000	EValuateLIST(list of quoted S-expressions)
05100		EVLIST(list  of  quoted S-expressions) generates an assertion
05200	that the list of the expressions has its value.   Thus  EVLIST('A,'(A
05300	B),'C) generates
05400		LIST('A,'(A B),'C)='(A (A B) C).
05500	
05600	EValuateEVAL(sexp)
05700		EVEVAL(sexp)  generates  an assertion that EVAL(sexp) has the
05800	value given it by the LISP evaluator.  A censor is supposed to  check
05900	that the evaluation of sexp involves only pure LISP functions and not
06000	any pseudo-functions with side  effects  like  SETQ's  and  RPLACA's.
06100	However,  the censor isn't working yet.  Thus EVEVAL('(CADR (QUOTE (A
06200	B))) generates
06300		EVAL('(CADR (QUOTE (A B)))='B.
06400	
06500	INTegerQUOTE(integer)
06600		INTQUOTE(integer) generates  an  assertion  that  integer  is
06700	equal to the integer quoted.  This gets around the fact that integers
06800	unlike  other  atoms  in  LISP  don't  have  to  be   quoted.    Thus
06900	INTQUOTE(27) generates
07000		27='27.  Needless  to  say,  INTQUOTE  balks  at  non-integer
07100	arguments.
07200	
07300	ISINTeger(integer)
07400		ISINT(integer)  generates  an  assertion  that  the  argument
07500	belongs  to  the  set  of  integers  if  this  is so.  Thus ISINT(27)
07600	generates
07700		27εI and ISINT(A) generates an error message.
07800	
07900		The  utility  of  these  commands  may  not be obvious to the
08000	meanest intelligence and will be demonstrated in a subsequent memo.
08100	
08200		RLISP programs for implementing these commands resides on the
08300	files  PCHECK.M1  and  PCHECK.M2 on [226,JMC] and may be added to any
08400	current version of PCHECK by using the IN command  of  RLISP  at  the
08500	command  level  of  the  proof checker.  A saved version of the proof
08600	checker  containing  these  commands  may  or  may   not   exist   as
08700	PCHECK.JMC[226,JMC].    Eventually,  these  commands  or  an  updated
08800	version thereof will be incorporated directly in PCHECK.